'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, f(ok(X)) -> ok(f(X))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, top(mark(X)) -> top(proper(X))
, top(ok(X)) -> top(active(X))}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ active^#(f(X)) -> c_0(if^#(X, c(), f(true())))
, active^#(if(true(), X, Y)) -> c_1()
, active^#(if(false(), X, Y)) -> c_2()
, active^#(f(X)) -> c_3(f^#(active(X)))
, active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))
, active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))
, f^#(mark(X)) -> c_6(f^#(X))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))
, proper^#(f(X)) -> c_9(f^#(proper(X)))
, proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))
, proper^#(c()) -> c_11()
, proper^#(true()) -> c_12()
, proper^#(false()) -> c_13()
, f^#(ok(X)) -> c_14(f^#(X))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, top^#(mark(X)) -> c_16(top^#(proper(X)))
, top^#(ok(X)) -> c_17(top^#(active(X)))}
The usable rules are:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
The estimated dependency graph contains the following edges:
{active^#(f(X)) -> c_0(if^#(X, c(), f(true())))}
==> {if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
{active^#(f(X)) -> c_3(f^#(active(X)))}
==> {f^#(ok(X)) -> c_14(f^#(X))}
{active^#(f(X)) -> c_3(f^#(active(X)))}
==> {f^#(mark(X)) -> c_6(f^#(X))}
{active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))}
==> {if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
{active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))}
==> {if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
{active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))}
==> {if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
{active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))}
==> {if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
{active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))}
==> {if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
{active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))}
==> {if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
{f^#(mark(X)) -> c_6(f^#(X))}
==> {f^#(ok(X)) -> c_14(f^#(X))}
{f^#(mark(X)) -> c_6(f^#(X))}
==> {f^#(mark(X)) -> c_6(f^#(X))}
{if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
==> {if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
{if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
==> {if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
{if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
==> {if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
{if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
==> {if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
{if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
==> {if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
{if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
==> {if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
{proper^#(f(X)) -> c_9(f^#(proper(X)))}
==> {f^#(ok(X)) -> c_14(f^#(X))}
{proper^#(f(X)) -> c_9(f^#(proper(X)))}
==> {f^#(mark(X)) -> c_6(f^#(X))}
{proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))}
==> {if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
{proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))}
==> {if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
{proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))}
==> {if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
{f^#(ok(X)) -> c_14(f^#(X))}
==> {f^#(ok(X)) -> c_14(f^#(X))}
{f^#(ok(X)) -> c_14(f^#(X))}
==> {f^#(mark(X)) -> c_6(f^#(X))}
{if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
==> {if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
{if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
==> {if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
{if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
==> {if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
{top^#(mark(X)) -> c_16(top^#(proper(X)))}
==> {top^#(ok(X)) -> c_17(top^#(active(X)))}
{top^#(mark(X)) -> c_16(top^#(proper(X)))}
==> {top^#(mark(X)) -> c_16(top^#(proper(X)))}
{top^#(ok(X)) -> c_17(top^#(active(X)))}
==> {top^#(ok(X)) -> c_17(top^#(active(X)))}
{top^#(ok(X)) -> c_17(top^#(active(X)))}
==> {top^#(mark(X)) -> c_16(top^#(proper(X)))}
We consider the following path(s):
1) { top^#(mark(X)) -> c_16(top^#(proper(X)))
, top^#(ok(X)) -> c_17(top^#(active(X)))}
The usable rules for this path are the following:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, top^#(mark(X)) -> c_16(top^#(proper(X)))
, top^#(ok(X)) -> c_17(top^#(active(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [0]
c_16(x1) = [1] x1 + [0]
c_17(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())}
and weakly orienting the rules
{if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [1] x1 + [5]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [0]
c_16(x1) = [1] x1 + [0]
c_17(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{top^#(ok(X)) -> c_17(top^#(active(X)))}
and weakly orienting the rules
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{top^#(ok(X)) -> c_17(top^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [1] x1 + [5]
ok(x1) = [1] x1 + [5]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [1]
c_16(x1) = [1] x1 + [0]
c_17(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(if(true(), X, Y)) -> mark(X)}
and weakly orienting the rules
{ top^#(ok(X)) -> c_17(top^#(active(X)))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(if(true(), X, Y)) -> mark(X)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [8]
false() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [0]
c_16(x1) = [1] x1 + [0]
c_17(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(if(false(), X, Y)) -> mark(Y)}
and weakly orienting the rules
{ active(if(true(), X, Y)) -> mark(X)
, top^#(ok(X)) -> c_17(top^#(active(X)))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(if(false(), X, Y)) -> mark(Y)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [4]
mark(x1) = [1] x1 + [10]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [8]
c() = [14]
true() = [1]
false() = [4]
proper(x1) = [1] x1 + [10]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [0]
c_16(x1) = [1] x1 + [3]
c_17(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{top^#(mark(X)) -> c_16(top^#(proper(X)))}
and weakly orienting the rules
{ active(if(false(), X, Y)) -> mark(Y)
, active(if(true(), X, Y)) -> mark(X)
, top^#(ok(X)) -> c_17(top^#(active(X)))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{top^#(mark(X)) -> c_16(top^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [5]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [8]
c() = [0]
true() = [8]
false() = [2]
proper(x1) = [1] x1 + [2]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [7]
c_16(x1) = [1] x1 + [0]
c_17(x1) = [1] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ top^#(mark(X)) -> c_16(top^#(proper(X)))
, active(if(false(), X, Y)) -> mark(Y)
, active(if(true(), X, Y)) -> mark(X)
, top^#(ok(X)) -> c_17(top^#(active(X)))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ top^#(mark(X)) -> c_16(top^#(proper(X)))
, active(if(false(), X, Y)) -> mark(Y)
, active(if(true(), X, Y)) -> mark(X)
, top^#(ok(X)) -> c_17(top^#(active(X)))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ active_0(2) -> 6
, mark_0(2) -> 2
, c_0() -> 2
, true_0() -> 2
, false_0() -> 2
, proper_0(2) -> 4
, ok_0(2) -> 2
, ok_0(2) -> 4
, top^#_0(2) -> 1
, top^#_0(4) -> 3
, top^#_0(6) -> 5
, c_16_0(3) -> 1
, c_17_0(5) -> 1
, c_17_0(5) -> 3}
2) { active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
The usable rules for this path are the following:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
Details:
We apply the weight gap principle, strictly orienting the rules
{if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [1] x1 + [1]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
and weakly orienting the rules
{if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
and weakly orienting the rules
{ if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [1] x1 + [1]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))}
and weakly orienting the rules
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [1] x1 + [1]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)}
and weakly orienting the rules
{ active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [4]
mark(x1) = [1] x1 + [5]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [6]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [14]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [2]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [1] x1 + [1]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(f(X)) -> mark(if(X, c(), f(true())))}
and weakly orienting the rules
{ active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(f(X)) -> mark(if(X, c(), f(true())))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [9]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [1]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [2]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [13]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(2) -> 2
, c_0() -> 2
, true_0() -> 2
, false_0() -> 2
, ok_0(2) -> 2
, active^#_0(2) -> 1
, if^#_0(2, 2, 2) -> 1
, c_7_0(1) -> 1
, c_8_0(1) -> 1
, c_15_0(1) -> 1}
3) { active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
The usable rules for this path are the following:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
Details:
We apply the weight gap principle, strictly orienting the rules
{if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [1] x1 + [1]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
and weakly orienting the rules
{if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
and weakly orienting the rules
{ if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [1] x1 + [1]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))}
and weakly orienting the rules
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [1] x1 + [1]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)}
and weakly orienting the rules
{ active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [4]
mark(x1) = [1] x1 + [5]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [6]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [14]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [2]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [1] x1 + [1]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(f(X)) -> mark(if(X, c(), f(true())))}
and weakly orienting the rules
{ active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(f(X)) -> mark(if(X, c(), f(true())))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [9]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [1]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [2]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [13]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(2) -> 2
, c_0() -> 2
, true_0() -> 2
, false_0() -> 2
, ok_0(2) -> 2
, active^#_0(2) -> 1
, if^#_0(2, 2, 2) -> 1
, c_7_0(1) -> 1
, c_8_0(1) -> 1
, c_15_0(1) -> 1}
4) { active^#(f(X)) -> c_3(f^#(active(X)))
, f^#(ok(X)) -> c_14(f^#(X))
, f^#(mark(X)) -> c_6(f^#(X))}
The usable rules for this path are the following:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(f(X)) -> c_3(f^#(active(X)))
, f^#(ok(X)) -> c_14(f^#(X))
, f^#(mark(X)) -> c_6(f^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [4]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [1] x1 + [1]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, f^#(ok(X)) -> c_14(f^#(X))}
and weakly orienting the rules
{ active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, f^#(ok(X)) -> c_14(f^#(X))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [12]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [1] x1 + [1]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(mark(X)) -> c_6(f^#(X))}
and weakly orienting the rules
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, f^#(ok(X)) -> c_14(f^#(X))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(mark(X)) -> c_6(f^#(X))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [1] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active^#(f(X)) -> c_3(f^#(active(X)))}
and weakly orienting the rules
{ f^#(mark(X)) -> c_6(f^#(X))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, f^#(ok(X)) -> c_14(f^#(X))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(f(X)) -> c_3(f^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [3]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [1] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(f(X)) -> mark(if(X, c(), f(true())))}
and weakly orienting the rules
{ active^#(f(X)) -> c_3(f^#(active(X)))
, f^#(mark(X)) -> c_6(f^#(X))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, f^#(ok(X)) -> c_14(f^#(X))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(f(X)) -> mark(if(X, c(), f(true())))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [6]
f(x1) = [1] x1 + [10]
mark(x1) = [1] x1 + [0]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [1]
false() = [9]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [7]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [13]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [14]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [1] x1 + [5]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active^#(f(X)) -> c_3(f^#(active(X)))
, f^#(mark(X)) -> c_6(f^#(X))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, f^#(ok(X)) -> c_14(f^#(X))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active^#(f(X)) -> c_3(f^#(active(X)))
, f^#(mark(X)) -> c_6(f^#(X))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, f^#(ok(X)) -> c_14(f^#(X))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(6) -> 3
, mark_0(7) -> 3
, mark_0(9) -> 3
, c_0() -> 5
, true_0() -> 6
, false_0() -> 7
, ok_0(3) -> 9
, ok_0(5) -> 9
, ok_0(6) -> 9
, ok_0(7) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(5) -> 11
, active^#_0(6) -> 11
, active^#_0(7) -> 11
, active^#_0(9) -> 11
, f^#_0(3) -> 17
, f^#_0(5) -> 17
, f^#_0(6) -> 17
, f^#_0(7) -> 17
, f^#_0(9) -> 17
, c_6_0(17) -> 17
, c_14_0(17) -> 17}
5) { proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [1] x1 + [1]
proper^#(x1) = [1] x1 + [1]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
and weakly orienting the rules
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [4]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [1] x1 + [1]
proper^#(x1) = [1] x1 + [1]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))}
and weakly orienting the rules
{ if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())}
and weakly orienting the rules
{ proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [1]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [13]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [8]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(2) -> 2
, c_0() -> 2
, true_0() -> 2
, false_0() -> 2
, ok_0(2) -> 2
, if^#_0(2, 2, 2) -> 1
, c_7_0(1) -> 1
, c_8_0(1) -> 1
, proper^#_0(2) -> 1
, c_15_0(1) -> 1}
6) { proper^#(f(X)) -> c_9(f^#(proper(X)))
, f^#(ok(X)) -> c_14(f^#(X))
, f^#(mark(X)) -> c_6(f^#(X))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, proper^#(f(X)) -> c_9(f^#(proper(X)))
, f^#(ok(X)) -> c_14(f^#(X))
, f^#(mark(X)) -> c_6(f^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [1] x1 + [1]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(f(X)) -> c_9(f^#(proper(X)))}
and weakly orienting the rules
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(f(X)) -> c_9(f^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [8]
true() = [0]
false() = [3]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [2]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [9]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [1] x1 + [9]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, f^#(mark(X)) -> c_6(f^#(X))}
and weakly orienting the rules
{ proper^#(f(X)) -> c_9(f^#(proper(X)))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, f^#(mark(X)) -> c_6(f^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [10]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [4]
c() = [5]
true() = [8]
false() = [5]
proper(x1) = [1] x1 + [9]
ok(x1) = [1] x1 + [6]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [2]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [13]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [1] x1 + [9]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(ok(X)) -> c_14(f^#(X))}
and weakly orienting the rules
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, f^#(mark(X)) -> c_6(f^#(X))
, proper^#(f(X)) -> c_9(f^#(proper(X)))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(ok(X)) -> c_14(f^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]
c() = [4]
true() = [0]
false() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [7]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [1] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ f^#(ok(X)) -> c_14(f^#(X))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, f^#(mark(X)) -> c_6(f^#(X))
, proper^#(f(X)) -> c_9(f^#(proper(X)))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ f^#(ok(X)) -> c_14(f^#(X))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, f^#(mark(X)) -> c_6(f^#(X))
, proper^#(f(X)) -> c_9(f^#(proper(X)))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(6) -> 3
, mark_0(7) -> 3
, mark_0(9) -> 3
, c_0() -> 5
, true_0() -> 6
, false_0() -> 7
, ok_0(3) -> 9
, ok_0(5) -> 9
, ok_0(6) -> 9
, ok_0(7) -> 9
, ok_0(9) -> 9
, f^#_0(3) -> 17
, f^#_0(5) -> 17
, f^#_0(6) -> 17
, f^#_0(7) -> 17
, f^#_0(9) -> 17
, c_6_0(17) -> 17
, proper^#_0(3) -> 23
, proper^#_0(5) -> 23
, proper^#_0(6) -> 23
, proper^#_0(7) -> 23
, proper^#_0(9) -> 23
, c_14_0(17) -> 17}
7) {active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))}
The usable rules for this path are the following:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [3]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [1]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
and weakly orienting the rules
{active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [2]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [4]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)}
and weakly orienting the rules
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [15]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(f(X)) -> mark(if(X, c(), f(true())))}
and weakly orienting the rules
{ active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(f(X)) -> mark(if(X, c(), f(true())))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [5]
f(x1) = [1] x1 + [4]
mark(x1) = [1] x1 + [4]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [12]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [5]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(6) -> 3
, mark_0(7) -> 3
, mark_0(9) -> 3
, c_0() -> 5
, true_0() -> 6
, false_0() -> 7
, ok_0(3) -> 9
, ok_0(5) -> 9
, ok_0(6) -> 9
, ok_0(7) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(5) -> 11
, active^#_0(6) -> 11
, active^#_0(7) -> 11
, active^#_0(9) -> 11
, if^#_0(3, 3, 3) -> 13
, if^#_0(3, 3, 5) -> 13
, if^#_0(3, 3, 6) -> 13
, if^#_0(3, 3, 7) -> 13
, if^#_0(3, 3, 9) -> 13
, if^#_0(3, 5, 3) -> 13
, if^#_0(3, 5, 5) -> 13
, if^#_0(3, 5, 6) -> 13
, if^#_0(3, 5, 7) -> 13
, if^#_0(3, 5, 9) -> 13
, if^#_0(3, 6, 3) -> 13
, if^#_0(3, 6, 5) -> 13
, if^#_0(3, 6, 6) -> 13
, if^#_0(3, 6, 7) -> 13
, if^#_0(3, 6, 9) -> 13
, if^#_0(3, 7, 3) -> 13
, if^#_0(3, 7, 5) -> 13
, if^#_0(3, 7, 6) -> 13
, if^#_0(3, 7, 7) -> 13
, if^#_0(3, 7, 9) -> 13
, if^#_0(3, 9, 3) -> 13
, if^#_0(3, 9, 5) -> 13
, if^#_0(3, 9, 6) -> 13
, if^#_0(3, 9, 7) -> 13
, if^#_0(3, 9, 9) -> 13
, if^#_0(5, 3, 3) -> 13
, if^#_0(5, 3, 5) -> 13
, if^#_0(5, 3, 6) -> 13
, if^#_0(5, 3, 7) -> 13
, if^#_0(5, 3, 9) -> 13
, if^#_0(5, 5, 3) -> 13
, if^#_0(5, 5, 5) -> 13
, if^#_0(5, 5, 6) -> 13
, if^#_0(5, 5, 7) -> 13
, if^#_0(5, 5, 9) -> 13
, if^#_0(5, 6, 3) -> 13
, if^#_0(5, 6, 5) -> 13
, if^#_0(5, 6, 6) -> 13
, if^#_0(5, 6, 7) -> 13
, if^#_0(5, 6, 9) -> 13
, if^#_0(5, 7, 3) -> 13
, if^#_0(5, 7, 5) -> 13
, if^#_0(5, 7, 6) -> 13
, if^#_0(5, 7, 7) -> 13
, if^#_0(5, 7, 9) -> 13
, if^#_0(5, 9, 3) -> 13
, if^#_0(5, 9, 5) -> 13
, if^#_0(5, 9, 6) -> 13
, if^#_0(5, 9, 7) -> 13
, if^#_0(5, 9, 9) -> 13
, if^#_0(6, 3, 3) -> 13
, if^#_0(6, 3, 5) -> 13
, if^#_0(6, 3, 6) -> 13
, if^#_0(6, 3, 7) -> 13
, if^#_0(6, 3, 9) -> 13
, if^#_0(6, 5, 3) -> 13
, if^#_0(6, 5, 5) -> 13
, if^#_0(6, 5, 6) -> 13
, if^#_0(6, 5, 7) -> 13
, if^#_0(6, 5, 9) -> 13
, if^#_0(6, 6, 3) -> 13
, if^#_0(6, 6, 5) -> 13
, if^#_0(6, 6, 6) -> 13
, if^#_0(6, 6, 7) -> 13
, if^#_0(6, 6, 9) -> 13
, if^#_0(6, 7, 3) -> 13
, if^#_0(6, 7, 5) -> 13
, if^#_0(6, 7, 6) -> 13
, if^#_0(6, 7, 7) -> 13
, if^#_0(6, 7, 9) -> 13
, if^#_0(6, 9, 3) -> 13
, if^#_0(6, 9, 5) -> 13
, if^#_0(6, 9, 6) -> 13
, if^#_0(6, 9, 7) -> 13
, if^#_0(6, 9, 9) -> 13
, if^#_0(7, 3, 3) -> 13
, if^#_0(7, 3, 5) -> 13
, if^#_0(7, 3, 6) -> 13
, if^#_0(7, 3, 7) -> 13
, if^#_0(7, 3, 9) -> 13
, if^#_0(7, 5, 3) -> 13
, if^#_0(7, 5, 5) -> 13
, if^#_0(7, 5, 6) -> 13
, if^#_0(7, 5, 7) -> 13
, if^#_0(7, 5, 9) -> 13
, if^#_0(7, 6, 3) -> 13
, if^#_0(7, 6, 5) -> 13
, if^#_0(7, 6, 6) -> 13
, if^#_0(7, 6, 7) -> 13
, if^#_0(7, 6, 9) -> 13
, if^#_0(7, 7, 3) -> 13
, if^#_0(7, 7, 5) -> 13
, if^#_0(7, 7, 6) -> 13
, if^#_0(7, 7, 7) -> 13
, if^#_0(7, 7, 9) -> 13
, if^#_0(7, 9, 3) -> 13
, if^#_0(7, 9, 5) -> 13
, if^#_0(7, 9, 6) -> 13
, if^#_0(7, 9, 7) -> 13
, if^#_0(7, 9, 9) -> 13
, if^#_0(9, 3, 3) -> 13
, if^#_0(9, 3, 5) -> 13
, if^#_0(9, 3, 6) -> 13
, if^#_0(9, 3, 7) -> 13
, if^#_0(9, 3, 9) -> 13
, if^#_0(9, 5, 3) -> 13
, if^#_0(9, 5, 5) -> 13
, if^#_0(9, 5, 6) -> 13
, if^#_0(9, 5, 7) -> 13
, if^#_0(9, 5, 9) -> 13
, if^#_0(9, 6, 3) -> 13
, if^#_0(9, 6, 5) -> 13
, if^#_0(9, 6, 6) -> 13
, if^#_0(9, 6, 7) -> 13
, if^#_0(9, 6, 9) -> 13
, if^#_0(9, 7, 3) -> 13
, if^#_0(9, 7, 5) -> 13
, if^#_0(9, 7, 6) -> 13
, if^#_0(9, 7, 7) -> 13
, if^#_0(9, 7, 9) -> 13
, if^#_0(9, 9, 3) -> 13
, if^#_0(9, 9, 5) -> 13
, if^#_0(9, 9, 6) -> 13
, if^#_0(9, 9, 7) -> 13
, if^#_0(9, 9, 9) -> 13}
8) {active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))}
The usable rules for this path are the following:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [3]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
and weakly orienting the rules
{active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [2]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [4]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)}
and weakly orienting the rules
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [15]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(f(X)) -> mark(if(X, c(), f(true())))}
and weakly orienting the rules
{ active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(f(X)) -> mark(if(X, c(), f(true())))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [5]
f(x1) = [1] x1 + [4]
mark(x1) = [1] x1 + [4]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [12]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [5]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(if(X1, X2, X3)) -> c_5(if^#(X1, active(X2), X3))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(6) -> 3
, mark_0(7) -> 3
, mark_0(9) -> 3
, c_0() -> 5
, true_0() -> 6
, false_0() -> 7
, ok_0(3) -> 9
, ok_0(5) -> 9
, ok_0(6) -> 9
, ok_0(7) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(5) -> 11
, active^#_0(6) -> 11
, active^#_0(7) -> 11
, active^#_0(9) -> 11
, if^#_0(3, 3, 3) -> 13
, if^#_0(3, 3, 5) -> 13
, if^#_0(3, 3, 6) -> 13
, if^#_0(3, 3, 7) -> 13
, if^#_0(3, 3, 9) -> 13
, if^#_0(3, 5, 3) -> 13
, if^#_0(3, 5, 5) -> 13
, if^#_0(3, 5, 6) -> 13
, if^#_0(3, 5, 7) -> 13
, if^#_0(3, 5, 9) -> 13
, if^#_0(3, 6, 3) -> 13
, if^#_0(3, 6, 5) -> 13
, if^#_0(3, 6, 6) -> 13
, if^#_0(3, 6, 7) -> 13
, if^#_0(3, 6, 9) -> 13
, if^#_0(3, 7, 3) -> 13
, if^#_0(3, 7, 5) -> 13
, if^#_0(3, 7, 6) -> 13
, if^#_0(3, 7, 7) -> 13
, if^#_0(3, 7, 9) -> 13
, if^#_0(3, 9, 3) -> 13
, if^#_0(3, 9, 5) -> 13
, if^#_0(3, 9, 6) -> 13
, if^#_0(3, 9, 7) -> 13
, if^#_0(3, 9, 9) -> 13
, if^#_0(5, 3, 3) -> 13
, if^#_0(5, 3, 5) -> 13
, if^#_0(5, 3, 6) -> 13
, if^#_0(5, 3, 7) -> 13
, if^#_0(5, 3, 9) -> 13
, if^#_0(5, 5, 3) -> 13
, if^#_0(5, 5, 5) -> 13
, if^#_0(5, 5, 6) -> 13
, if^#_0(5, 5, 7) -> 13
, if^#_0(5, 5, 9) -> 13
, if^#_0(5, 6, 3) -> 13
, if^#_0(5, 6, 5) -> 13
, if^#_0(5, 6, 6) -> 13
, if^#_0(5, 6, 7) -> 13
, if^#_0(5, 6, 9) -> 13
, if^#_0(5, 7, 3) -> 13
, if^#_0(5, 7, 5) -> 13
, if^#_0(5, 7, 6) -> 13
, if^#_0(5, 7, 7) -> 13
, if^#_0(5, 7, 9) -> 13
, if^#_0(5, 9, 3) -> 13
, if^#_0(5, 9, 5) -> 13
, if^#_0(5, 9, 6) -> 13
, if^#_0(5, 9, 7) -> 13
, if^#_0(5, 9, 9) -> 13
, if^#_0(6, 3, 3) -> 13
, if^#_0(6, 3, 5) -> 13
, if^#_0(6, 3, 6) -> 13
, if^#_0(6, 3, 7) -> 13
, if^#_0(6, 3, 9) -> 13
, if^#_0(6, 5, 3) -> 13
, if^#_0(6, 5, 5) -> 13
, if^#_0(6, 5, 6) -> 13
, if^#_0(6, 5, 7) -> 13
, if^#_0(6, 5, 9) -> 13
, if^#_0(6, 6, 3) -> 13
, if^#_0(6, 6, 5) -> 13
, if^#_0(6, 6, 6) -> 13
, if^#_0(6, 6, 7) -> 13
, if^#_0(6, 6, 9) -> 13
, if^#_0(6, 7, 3) -> 13
, if^#_0(6, 7, 5) -> 13
, if^#_0(6, 7, 6) -> 13
, if^#_0(6, 7, 7) -> 13
, if^#_0(6, 7, 9) -> 13
, if^#_0(6, 9, 3) -> 13
, if^#_0(6, 9, 5) -> 13
, if^#_0(6, 9, 6) -> 13
, if^#_0(6, 9, 7) -> 13
, if^#_0(6, 9, 9) -> 13
, if^#_0(7, 3, 3) -> 13
, if^#_0(7, 3, 5) -> 13
, if^#_0(7, 3, 6) -> 13
, if^#_0(7, 3, 7) -> 13
, if^#_0(7, 3, 9) -> 13
, if^#_0(7, 5, 3) -> 13
, if^#_0(7, 5, 5) -> 13
, if^#_0(7, 5, 6) -> 13
, if^#_0(7, 5, 7) -> 13
, if^#_0(7, 5, 9) -> 13
, if^#_0(7, 6, 3) -> 13
, if^#_0(7, 6, 5) -> 13
, if^#_0(7, 6, 6) -> 13
, if^#_0(7, 6, 7) -> 13
, if^#_0(7, 6, 9) -> 13
, if^#_0(7, 7, 3) -> 13
, if^#_0(7, 7, 5) -> 13
, if^#_0(7, 7, 6) -> 13
, if^#_0(7, 7, 7) -> 13
, if^#_0(7, 7, 9) -> 13
, if^#_0(7, 9, 3) -> 13
, if^#_0(7, 9, 5) -> 13
, if^#_0(7, 9, 6) -> 13
, if^#_0(7, 9, 7) -> 13
, if^#_0(7, 9, 9) -> 13
, if^#_0(9, 3, 3) -> 13
, if^#_0(9, 3, 5) -> 13
, if^#_0(9, 3, 6) -> 13
, if^#_0(9, 3, 7) -> 13
, if^#_0(9, 3, 9) -> 13
, if^#_0(9, 5, 3) -> 13
, if^#_0(9, 5, 5) -> 13
, if^#_0(9, 5, 6) -> 13
, if^#_0(9, 5, 7) -> 13
, if^#_0(9, 5, 9) -> 13
, if^#_0(9, 6, 3) -> 13
, if^#_0(9, 6, 5) -> 13
, if^#_0(9, 6, 6) -> 13
, if^#_0(9, 6, 7) -> 13
, if^#_0(9, 6, 9) -> 13
, if^#_0(9, 7, 3) -> 13
, if^#_0(9, 7, 5) -> 13
, if^#_0(9, 7, 6) -> 13
, if^#_0(9, 7, 7) -> 13
, if^#_0(9, 7, 9) -> 13
, if^#_0(9, 9, 3) -> 13
, if^#_0(9, 9, 5) -> 13
, if^#_0(9, 9, 6) -> 13
, if^#_0(9, 9, 7) -> 13
, if^#_0(9, 9, 9) -> 13}
9) {active^#(f(X)) -> c_3(f^#(active(X)))}
The usable rules for this path are the following:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(f(X)) -> c_3(f^#(active(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(f(X)) -> c_3(f^#(active(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(f(X)) -> c_3(f^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
and weakly orienting the rules
{active^#(f(X)) -> c_3(f^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [1] x1 + [8]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(if(false(), X, Y)) -> mark(Y)}
and weakly orienting the rules
{ if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(f(X)) -> c_3(f^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(if(false(), X, Y)) -> mark(Y)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [12]
mark(x1) = [1] x1 + [1]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [8]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [3]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [4]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)}
and weakly orienting the rules
{ active(if(false(), X, Y)) -> mark(Y)
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(f(X)) -> c_3(f^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(f(X)) -> c_3(f^#(active(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
, active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ active(f(X)) -> mark(if(X, c(), f(true())))
, active(if(true(), X, Y)) -> mark(X)
, active(if(false(), X, Y)) -> mark(Y)
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, active^#(f(X)) -> c_3(f^#(active(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(6) -> 3
, mark_0(7) -> 3
, mark_0(9) -> 3
, c_0() -> 5
, true_0() -> 6
, false_0() -> 7
, ok_0(3) -> 9
, ok_0(5) -> 9
, ok_0(6) -> 9
, ok_0(7) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(5) -> 11
, active^#_0(6) -> 11
, active^#_0(7) -> 11
, active^#_0(9) -> 11
, f^#_0(3) -> 17
, f^#_0(5) -> 17
, f^#_0(6) -> 17
, f^#_0(7) -> 17
, f^#_0(9) -> 17}
10)
{proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [4]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))}
and weakly orienting the rules
{if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [4]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())}
and weakly orienting the rules
{ proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [15]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [1]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, proper^#(if(X1, X2, X3)) ->
c_10(if^#(proper(X1), proper(X2), proper(X3)))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(6) -> 3
, mark_0(7) -> 3
, mark_0(9) -> 3
, c_0() -> 5
, true_0() -> 6
, false_0() -> 7
, ok_0(3) -> 9
, ok_0(5) -> 9
, ok_0(6) -> 9
, ok_0(7) -> 9
, ok_0(9) -> 9
, if^#_0(3, 3, 3) -> 13
, if^#_0(3, 3, 5) -> 13
, if^#_0(3, 3, 6) -> 13
, if^#_0(3, 3, 7) -> 13
, if^#_0(3, 3, 9) -> 13
, if^#_0(3, 5, 3) -> 13
, if^#_0(3, 5, 5) -> 13
, if^#_0(3, 5, 6) -> 13
, if^#_0(3, 5, 7) -> 13
, if^#_0(3, 5, 9) -> 13
, if^#_0(3, 6, 3) -> 13
, if^#_0(3, 6, 5) -> 13
, if^#_0(3, 6, 6) -> 13
, if^#_0(3, 6, 7) -> 13
, if^#_0(3, 6, 9) -> 13
, if^#_0(3, 7, 3) -> 13
, if^#_0(3, 7, 5) -> 13
, if^#_0(3, 7, 6) -> 13
, if^#_0(3, 7, 7) -> 13
, if^#_0(3, 7, 9) -> 13
, if^#_0(3, 9, 3) -> 13
, if^#_0(3, 9, 5) -> 13
, if^#_0(3, 9, 6) -> 13
, if^#_0(3, 9, 7) -> 13
, if^#_0(3, 9, 9) -> 13
, if^#_0(5, 3, 3) -> 13
, if^#_0(5, 3, 5) -> 13
, if^#_0(5, 3, 6) -> 13
, if^#_0(5, 3, 7) -> 13
, if^#_0(5, 3, 9) -> 13
, if^#_0(5, 5, 3) -> 13
, if^#_0(5, 5, 5) -> 13
, if^#_0(5, 5, 6) -> 13
, if^#_0(5, 5, 7) -> 13
, if^#_0(5, 5, 9) -> 13
, if^#_0(5, 6, 3) -> 13
, if^#_0(5, 6, 5) -> 13
, if^#_0(5, 6, 6) -> 13
, if^#_0(5, 6, 7) -> 13
, if^#_0(5, 6, 9) -> 13
, if^#_0(5, 7, 3) -> 13
, if^#_0(5, 7, 5) -> 13
, if^#_0(5, 7, 6) -> 13
, if^#_0(5, 7, 7) -> 13
, if^#_0(5, 7, 9) -> 13
, if^#_0(5, 9, 3) -> 13
, if^#_0(5, 9, 5) -> 13
, if^#_0(5, 9, 6) -> 13
, if^#_0(5, 9, 7) -> 13
, if^#_0(5, 9, 9) -> 13
, if^#_0(6, 3, 3) -> 13
, if^#_0(6, 3, 5) -> 13
, if^#_0(6, 3, 6) -> 13
, if^#_0(6, 3, 7) -> 13
, if^#_0(6, 3, 9) -> 13
, if^#_0(6, 5, 3) -> 13
, if^#_0(6, 5, 5) -> 13
, if^#_0(6, 5, 6) -> 13
, if^#_0(6, 5, 7) -> 13
, if^#_0(6, 5, 9) -> 13
, if^#_0(6, 6, 3) -> 13
, if^#_0(6, 6, 5) -> 13
, if^#_0(6, 6, 6) -> 13
, if^#_0(6, 6, 7) -> 13
, if^#_0(6, 6, 9) -> 13
, if^#_0(6, 7, 3) -> 13
, if^#_0(6, 7, 5) -> 13
, if^#_0(6, 7, 6) -> 13
, if^#_0(6, 7, 7) -> 13
, if^#_0(6, 7, 9) -> 13
, if^#_0(6, 9, 3) -> 13
, if^#_0(6, 9, 5) -> 13
, if^#_0(6, 9, 6) -> 13
, if^#_0(6, 9, 7) -> 13
, if^#_0(6, 9, 9) -> 13
, if^#_0(7, 3, 3) -> 13
, if^#_0(7, 3, 5) -> 13
, if^#_0(7, 3, 6) -> 13
, if^#_0(7, 3, 7) -> 13
, if^#_0(7, 3, 9) -> 13
, if^#_0(7, 5, 3) -> 13
, if^#_0(7, 5, 5) -> 13
, if^#_0(7, 5, 6) -> 13
, if^#_0(7, 5, 7) -> 13
, if^#_0(7, 5, 9) -> 13
, if^#_0(7, 6, 3) -> 13
, if^#_0(7, 6, 5) -> 13
, if^#_0(7, 6, 6) -> 13
, if^#_0(7, 6, 7) -> 13
, if^#_0(7, 6, 9) -> 13
, if^#_0(7, 7, 3) -> 13
, if^#_0(7, 7, 5) -> 13
, if^#_0(7, 7, 6) -> 13
, if^#_0(7, 7, 7) -> 13
, if^#_0(7, 7, 9) -> 13
, if^#_0(7, 9, 3) -> 13
, if^#_0(7, 9, 5) -> 13
, if^#_0(7, 9, 6) -> 13
, if^#_0(7, 9, 7) -> 13
, if^#_0(7, 9, 9) -> 13
, if^#_0(9, 3, 3) -> 13
, if^#_0(9, 3, 5) -> 13
, if^#_0(9, 3, 6) -> 13
, if^#_0(9, 3, 7) -> 13
, if^#_0(9, 3, 9) -> 13
, if^#_0(9, 5, 3) -> 13
, if^#_0(9, 5, 5) -> 13
, if^#_0(9, 5, 6) -> 13
, if^#_0(9, 5, 7) -> 13
, if^#_0(9, 5, 9) -> 13
, if^#_0(9, 6, 3) -> 13
, if^#_0(9, 6, 5) -> 13
, if^#_0(9, 6, 6) -> 13
, if^#_0(9, 6, 7) -> 13
, if^#_0(9, 6, 9) -> 13
, if^#_0(9, 7, 3) -> 13
, if^#_0(9, 7, 5) -> 13
, if^#_0(9, 7, 6) -> 13
, if^#_0(9, 7, 7) -> 13
, if^#_0(9, 7, 9) -> 13
, if^#_0(9, 9, 3) -> 13
, if^#_0(9, 9, 5) -> 13
, if^#_0(9, 9, 6) -> 13
, if^#_0(9, 9, 7) -> 13
, if^#_0(9, 9, 9) -> 13
, proper^#_0(3) -> 23
, proper^#_0(5) -> 23
, proper^#_0(6) -> 23
, proper^#_0(7) -> 23
, proper^#_0(9) -> 23}
11)
{proper^#(f(X)) -> c_9(f^#(proper(X)))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
, proper^#(f(X)) -> c_9(f^#(proper(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [4]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [9]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(f(X)) -> c_9(f^#(proper(X)))}
and weakly orienting the rules
{if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(f(X)) -> c_9(f^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())}
and weakly orienting the rules
{ proper^#(f(X)) -> c_9(f^#(proper(X)))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [15]
true() = [0]
false() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [4]
c_9(x1) = [1] x1 + [2]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, proper^#(f(X)) -> c_9(f^#(proper(X)))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
, if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))}
Weak Rules:
{ proper(c()) -> ok(c())
, proper(true()) -> ok(true())
, proper(false()) -> ok(false())
, proper^#(f(X)) -> c_9(f^#(proper(X)))
, if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(6) -> 3
, mark_0(7) -> 3
, mark_0(9) -> 3
, c_0() -> 5
, true_0() -> 6
, false_0() -> 7
, ok_0(3) -> 9
, ok_0(5) -> 9
, ok_0(6) -> 9
, ok_0(7) -> 9
, ok_0(9) -> 9
, f^#_0(3) -> 17
, f^#_0(5) -> 17
, f^#_0(6) -> 17
, f^#_0(7) -> 17
, f^#_0(9) -> 17
, proper^#_0(3) -> 23
, proper^#_0(5) -> 23
, proper^#_0(6) -> 23
, proper^#_0(7) -> 23
, proper^#_0(9) -> 23}
12)
{ active^#(f(X)) -> c_0(if^#(X, c(), f(true())))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
The usable rules for this path are the following:
{ f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, active^#(f(X)) -> c_0(if^#(X, c(), f(true())))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ active^#(f(X)) -> c_0(if^#(X, c(), f(true())))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active^#(f(X)) -> c_0(if^#(X, c(), f(true())))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [2]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c() = [2]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [2]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [3]
c_0(x1) = [1] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))}
Weak Rules:
{ active^#(f(X)) -> c_0(if^#(X, c(), f(true())))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))}
Weak Rules:
{ active^#(f(X)) -> c_0(if^#(X, c(), f(true())))
, if^#(mark(X1), X2, X3) -> c_7(if^#(X1, X2, X3))
, if^#(ok(X1), ok(X2), ok(X3)) -> c_15(if^#(X1, X2, X3))
, if^#(X1, mark(X2), X3) -> c_8(if^#(X1, X2, X3))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(2) -> 2
, c_0() -> 2
, true_0() -> 2
, ok_0(2) -> 2
, active^#_0(2) -> 1
, if^#_0(2, 2, 2) -> 1
, c_7_0(1) -> 1
, c_8_0(1) -> 1
, c_15_0(1) -> 1}
13)
{active^#(f(X)) -> c_0(if^#(X, c(), f(true())))}
The usable rules for this path are the following:
{ f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, active^#(f(X)) -> c_0(if^#(X, c(), f(true())))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(f(X)) -> c_0(if^#(X, c(), f(true())))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(f(X)) -> c_0(if^#(X, c(), f(true())))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [1]
mark(x1) = [1] x1 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c() = [1]
true() = [7]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [12]
c_0(x1) = [1] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))}
Weak Rules: {active^#(f(X)) -> c_0(if^#(X, c(), f(true())))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))}
Weak Rules: {active^#(f(X)) -> c_0(if^#(X, c(), f(true())))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(6) -> 3
, mark_0(9) -> 3
, c_0() -> 5
, true_0() -> 6
, ok_0(3) -> 9
, ok_0(5) -> 9
, ok_0(6) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(5) -> 11
, active^#_0(6) -> 11
, active^#_0(9) -> 11
, if^#_0(3, 3, 3) -> 13
, if^#_0(3, 3, 5) -> 13
, if^#_0(3, 3, 6) -> 13
, if^#_0(3, 3, 9) -> 13
, if^#_0(3, 5, 3) -> 13
, if^#_0(3, 5, 5) -> 13
, if^#_0(3, 5, 6) -> 13
, if^#_0(3, 5, 9) -> 13
, if^#_0(3, 6, 3) -> 13
, if^#_0(3, 6, 5) -> 13
, if^#_0(3, 6, 6) -> 13
, if^#_0(3, 6, 9) -> 13
, if^#_0(3, 9, 3) -> 13
, if^#_0(3, 9, 5) -> 13
, if^#_0(3, 9, 6) -> 13
, if^#_0(3, 9, 9) -> 13
, if^#_0(5, 3, 3) -> 13
, if^#_0(5, 3, 5) -> 13
, if^#_0(5, 3, 6) -> 13
, if^#_0(5, 3, 9) -> 13
, if^#_0(5, 5, 3) -> 13
, if^#_0(5, 5, 5) -> 13
, if^#_0(5, 5, 6) -> 13
, if^#_0(5, 5, 9) -> 13
, if^#_0(5, 6, 3) -> 13
, if^#_0(5, 6, 5) -> 13
, if^#_0(5, 6, 6) -> 13
, if^#_0(5, 6, 9) -> 13
, if^#_0(5, 9, 3) -> 13
, if^#_0(5, 9, 5) -> 13
, if^#_0(5, 9, 6) -> 13
, if^#_0(5, 9, 9) -> 13
, if^#_0(6, 3, 3) -> 13
, if^#_0(6, 3, 5) -> 13
, if^#_0(6, 3, 6) -> 13
, if^#_0(6, 3, 9) -> 13
, if^#_0(6, 5, 3) -> 13
, if^#_0(6, 5, 5) -> 13
, if^#_0(6, 5, 6) -> 13
, if^#_0(6, 5, 9) -> 13
, if^#_0(6, 6, 3) -> 13
, if^#_0(6, 6, 5) -> 13
, if^#_0(6, 6, 6) -> 13
, if^#_0(6, 6, 9) -> 13
, if^#_0(6, 9, 3) -> 13
, if^#_0(6, 9, 5) -> 13
, if^#_0(6, 9, 6) -> 13
, if^#_0(6, 9, 9) -> 13
, if^#_0(9, 3, 3) -> 13
, if^#_0(9, 3, 5) -> 13
, if^#_0(9, 3, 6) -> 13
, if^#_0(9, 3, 9) -> 13
, if^#_0(9, 5, 3) -> 13
, if^#_0(9, 5, 5) -> 13
, if^#_0(9, 5, 6) -> 13
, if^#_0(9, 5, 9) -> 13
, if^#_0(9, 6, 3) -> 13
, if^#_0(9, 6, 5) -> 13
, if^#_0(9, 6, 6) -> 13
, if^#_0(9, 6, 9) -> 13
, if^#_0(9, 9, 3) -> 13
, if^#_0(9, 9, 5) -> 13
, if^#_0(9, 9, 6) -> 13
, if^#_0(9, 9, 9) -> 13}
14)
{active^#(if(false(), X, Y)) -> c_2()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {active^#(if(false(), X, Y)) -> c_2()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(if(false(), X, Y)) -> c_2()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(if(false(), X, Y)) -> c_2()}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {active^#(if(false(), X, Y)) -> c_2()}
Details:
The given problem does not contain any strict rules
15)
{active^#(if(true(), X, Y)) -> c_1()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {active^#(if(true(), X, Y)) -> c_1()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(if(true(), X, Y)) -> c_1()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(if(true(), X, Y)) -> c_1()}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
if(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {active^#(if(true(), X, Y)) -> c_1()}
Details:
The given problem does not contain any strict rules
16)
{proper^#(true()) -> c_12()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {proper^#(true()) -> c_12()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(true()) -> c_12()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(true()) -> c_12()}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {proper^#(true()) -> c_12()}
Details:
The given problem does not contain any strict rules
17)
{proper^#(c()) -> c_11()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {proper^#(c()) -> c_11()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(c()) -> c_11()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(c()) -> c_11()}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {proper^#(c()) -> c_11()}
Details:
The given problem does not contain any strict rules
18)
{proper^#(false()) -> c_13()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {proper^#(false()) -> c_13()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(false()) -> c_13()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(false()) -> c_13()}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c() = [0]
true() = [0]
false() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_1() = [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11() = [0]
c_12() = [0]
c_13() = [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {proper^#(false()) -> c_13()}
Details:
The given problem does not contain any strict rules